nLab Feit-Thompson theorem

Statement

Theorem

Every finite group of odd order is a solvable group.

This is due to Feit & Thompson 1962.

A fully formalized proof in Coq has been produced by Gonthier et al. 2013.

References

The original proof:

• Walter Feit, John Thompson: A solvability criterion for finite groups and some consequences, Proc. Nat. Acad. Sci. 48 6 (1962) 968-970 [jstor:71265]

Formalization in Coq:

• Georges Gonthier et al.: A Machine-Checked Proof of the Odd Order Theorem, in: Interactive Theorem Proving. ITP 2013, Lecture Notes in Computer Science 7998, Springer (2013) [doi:10.1007/978-3-642-39634-2_14]